Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TOP(rec(up(x))) → REC(x)
CHECK(no(x)) → CHECK(x)
REC(bot) → SENT(bot)
REC(rec(x)) → SENT(rec(x))
TOP(sent(up(x))) → CHECK(rec(x))
CHECK(rec(x)) → CHECK(x)
REC(up(x)) → REC(x)
TOP(no(up(x))) → REC(x)
TOP(sent(up(x))) → TOP(check(rec(x)))
REC(no(x)) → SENT(rec(x))
CHECK(sent(x)) → SENT(check(x))
CHECK(rec(x)) → REC(check(x))
TOP(no(up(x))) → CHECK(rec(x))
CHECK(no(x)) → NO(check(x))
REC(sent(x)) → SENT(rec(x))
CHECK(up(x)) → CHECK(x)
TOP(sent(up(x))) → REC(x)
TOP(rec(up(x))) → CHECK(rec(x))
TOP(no(up(x))) → TOP(check(rec(x)))
REC(no(x)) → REC(x)
NO(up(x)) → NO(x)
SENT(up(x)) → SENT(x)
TOP(rec(up(x))) → TOP(check(rec(x)))
REC(sent(x)) → REC(x)
CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

TOP(rec(up(x))) → REC(x)
CHECK(no(x)) → CHECK(x)
REC(bot) → SENT(bot)
REC(rec(x)) → SENT(rec(x))
TOP(sent(up(x))) → CHECK(rec(x))
CHECK(rec(x)) → CHECK(x)
REC(up(x)) → REC(x)
TOP(no(up(x))) → REC(x)
TOP(sent(up(x))) → TOP(check(rec(x)))
REC(no(x)) → SENT(rec(x))
CHECK(sent(x)) → SENT(check(x))
CHECK(rec(x)) → REC(check(x))
TOP(no(up(x))) → CHECK(rec(x))
CHECK(no(x)) → NO(check(x))
REC(sent(x)) → SENT(rec(x))
CHECK(up(x)) → CHECK(x)
TOP(sent(up(x))) → REC(x)
TOP(rec(up(x))) → CHECK(rec(x))
TOP(no(up(x))) → TOP(check(rec(x)))
REC(no(x)) → REC(x)
NO(up(x)) → NO(x)
SENT(up(x)) → SENT(x)
TOP(rec(up(x))) → TOP(check(rec(x)))
REC(sent(x)) → REC(x)
CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

CHECK(no(x)) → CHECK(x)
TOP(rec(up(x))) → REC(x)
REC(bot) → SENT(bot)
REC(rec(x)) → SENT(rec(x))
CHECK(rec(x)) → CHECK(x)
TOP(sent(up(x))) → CHECK(rec(x))
REC(up(x)) → REC(x)
TOP(no(up(x))) → REC(x)
TOP(sent(up(x))) → TOP(check(rec(x)))
REC(no(x)) → SENT(rec(x))
CHECK(sent(x)) → SENT(check(x))
CHECK(rec(x)) → REC(check(x))
TOP(no(up(x))) → CHECK(rec(x))
CHECK(no(x)) → NO(check(x))
REC(sent(x)) → SENT(rec(x))
CHECK(up(x)) → CHECK(x)
TOP(sent(up(x))) → REC(x)
TOP(rec(up(x))) → CHECK(rec(x))
TOP(no(up(x))) → TOP(check(rec(x)))
REC(no(x)) → REC(x)
SENT(up(x)) → SENT(x)
NO(up(x)) → NO(x)
TOP(rec(up(x))) → TOP(check(rec(x)))
REC(sent(x)) → REC(x)
CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 5 SCCs with 13 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

NO(up(x)) → NO(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


NO(up(x)) → NO(x)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
NO(x1)  =  NO(x1)
up(x1)  =  up(x1)

Lexicographic path order with status [19].
Precedence:
up1 > NO1

Status:
NO1: [1]
up1: multiset

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SENT(up(x)) → SENT(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


SENT(up(x)) → SENT(x)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SENT(x1)  =  SENT(x1)
up(x1)  =  up(x1)

Lexicographic path order with status [19].
Precedence:
up1 > SENT1

Status:
up1: multiset
SENT1: [1]

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REC(up(x)) → REC(x)
REC(no(x)) → REC(x)
REC(sent(x)) → REC(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


REC(sent(x)) → REC(x)
The remaining pairs can at least be oriented weakly.

REC(up(x)) → REC(x)
REC(no(x)) → REC(x)
Used ordering: Combined order from the following AFS and order.
REC(x1)  =  REC(x1)
up(x1)  =  x1
no(x1)  =  x1
sent(x1)  =  sent(x1)

Lexicographic path order with status [19].
Precedence:
trivial

Status:
REC1: [1]
sent1: multiset

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REC(up(x)) → REC(x)
REC(no(x)) → REC(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


REC(up(x)) → REC(x)
The remaining pairs can at least be oriented weakly.

REC(no(x)) → REC(x)
Used ordering: Combined order from the following AFS and order.
REC(x1)  =  REC(x1)
up(x1)  =  up(x1)
no(x1)  =  x1

Lexicographic path order with status [19].
Precedence:
up1 > REC1

Status:
up1: multiset
REC1: [1]

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REC(no(x)) → REC(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


REC(no(x)) → REC(x)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
REC(x1)  =  REC(x1)
no(x1)  =  no(x1)

Lexicographic path order with status [19].
Precedence:
no1 > REC1

Status:
no1: multiset
REC1: [1]

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof
QDP
                            ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPOrderProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CHECK(no(x)) → CHECK(x)
CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


CHECK(no(x)) → CHECK(x)
The remaining pairs can at least be oriented weakly.

CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)
Used ordering: Combined order from the following AFS and order.
CHECK(x1)  =  CHECK(x1)
no(x1)  =  no(x1)
up(x1)  =  x1
sent(x1)  =  x1
rec(x1)  =  x1

Lexicographic path order with status [19].
Precedence:
no1 > CHECK1

Status:
no1: multiset
CHECK1: [1]

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ QDPOrderProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)
CHECK(rec(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


CHECK(rec(x)) → CHECK(x)
The remaining pairs can at least be oriented weakly.

CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)
Used ordering: Combined order from the following AFS and order.
CHECK(x1)  =  CHECK(x1)
up(x1)  =  x1
sent(x1)  =  x1
rec(x1)  =  rec(x1)

Lexicographic path order with status [19].
Precedence:
trivial

Status:
rec1: multiset
CHECK1: [1]

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ QDPOrderProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CHECK(up(x)) → CHECK(x)
CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


CHECK(up(x)) → CHECK(x)
The remaining pairs can at least be oriented weakly.

CHECK(sent(x)) → CHECK(x)
Used ordering: Combined order from the following AFS and order.
CHECK(x1)  =  CHECK(x1)
up(x1)  =  up(x1)
sent(x1)  =  x1

Lexicographic path order with status [19].
Precedence:
up1 > CHECK1

Status:
up1: multiset
CHECK1: [1]

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof
QDP
                            ↳ QDPOrderProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CHECK(sent(x)) → CHECK(x)

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


CHECK(sent(x)) → CHECK(x)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
CHECK(x1)  =  CHECK(x1)
sent(x1)  =  sent(x1)

Lexicographic path order with status [19].
Precedence:
sent1 > CHECK1

Status:
CHECK1: [1]
sent1: multiset

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ QDPOrderProof
QDP
                                ↳ PisEmptyProof
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(no(up(x))) → TOP(check(rec(x)))
TOP(sent(up(x))) → TOP(check(rec(x)))
TOP(rec(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


TOP(no(up(x))) → TOP(check(rec(x)))
The remaining pairs can at least be oriented weakly.

TOP(sent(up(x))) → TOP(check(rec(x)))
TOP(rec(up(x))) → TOP(check(rec(x)))
Used ordering: Combined order from the following AFS and order.
TOP(x1)  =  TOP(x1)
no(x1)  =  no(x1)
up(x1)  =  x1
check(x1)  =  x1
rec(x1)  =  x1
sent(x1)  =  x1
bot  =  bot

Lexicographic path order with status [19].
Precedence:
no1 > TOP1

Status:
no1: [1]
bot: multiset
TOP1: [1]

The following usable rules [14] were oriented:

rec(sent(x)) → sent(rec(x))
no(up(x)) → up(no(x))
check(no(x)) → no(x)
check(up(x)) → up(check(x))
rec(up(x)) → up(rec(x))
check(rec(x)) → rec(check(x))
rec(no(x)) → sent(rec(x))
check(sent(x)) → sent(check(x))
check(no(x)) → no(check(x))
sent(up(x)) → up(sent(x))
rec(bot) → up(sent(bot))
rec(rec(x)) → sent(rec(x))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP

Q DP problem:
The TRS P consists of the following rules:

TOP(sent(up(x))) → TOP(check(rec(x)))
TOP(rec(up(x))) → TOP(check(rec(x)))

The TRS R consists of the following rules:

rec(rec(x)) → sent(rec(x))
rec(sent(x)) → sent(rec(x))
rec(no(x)) → sent(rec(x))
rec(bot) → up(sent(bot))
rec(up(x)) → up(rec(x))
sent(up(x)) → up(sent(x))
no(up(x)) → up(no(x))
top(rec(up(x))) → top(check(rec(x)))
top(sent(up(x))) → top(check(rec(x)))
top(no(up(x))) → top(check(rec(x)))
check(up(x)) → up(check(x))
check(sent(x)) → sent(check(x))
check(rec(x)) → rec(check(x))
check(no(x)) → no(check(x))
check(no(x)) → no(x)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.